Nuprl Lemma : f-free-isrcv 11,40
es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Newround(e1)
  (j  L)
  ((j = loc(e1)))
  (isrcv(the rcv(free message from e1 to j)))) 
latex

Definitions, tt, True, if b then t else f fi , P  Q, P  Q, P & Q, t  T, IdLnk, "$x", the rcv(free message from e1 to j), isrcv(e), b, P  Q, Id, x:A. B(x), False, ff, eq_atom$n(x;y), Atom2Deq, IdDeq, t.1, eqof(d), a = b, x:A. B(x), xL. P(x), P  Q, A c B, Newround(e), fischer(L)
Lemmasevent system wf, fischer wf, es-E wf, f-newround wf, l member wf, es-loc wf, Id wf, not wf, assert-eq-id, es-kind-first-from

origin